(*
  Copyright (c) 2009 Barry Schwartz

  Permission is hereby granted, free of charge, to any person
  obtaining a copy of this software and associated documentation
  files (the "Software"), to deal in the Software without
  restriction, including without limitation the rights to use,
  copy, modify, merge, publish, distribute, sublicense, and/or sell
  copies of the Software, and to permit persons to whom the
  Software is furnished to do so, subject to the following
  conditions:

  The above copyright notice and this permission notice shall be
  included in all copies or substantial portions of the Software.

  THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
  EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
  OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
  NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
  HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
  WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
  FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
  OTHER DEALINGS IN THE SOFTWARE.
*)

open XNum
open VMTypes
open UTypes
open SymbolTable
  
let tracing_bytecode = ref false
  
module Environment =
  struct
    type environment = (unknown array) list
    
    let empty = []
      
    let push env arr = arr :: env
      
    let push_unbound env n = (Array.init n create_unbound) :: env
      
    let pop env =
      match env with
      | _ :: es -> es
      | [] -> runtime_error "empty environment"
      
    let lookup env lvl idx =
      let rec iter lvl env =
        match env with
        | [] -> assert false
        | e :: es -> if lvl <= 0 then e.(idx) else iter (lvl - 1) es
      in iter lvl env
      
    let set env lvl idx x =
      let rec iter lvl env =
        match env with
        | [] -> assert false
        | e :: es -> if lvl <= 0 then e.(idx) <- x else iter (lvl - 1) es
      in iter lvl env
      
  end
  
module Stack =
  struct
    let call_stack = ref []
      
    let value_stack = ref []
      
    let clear () = (call_stack := []; value_stack := [])
      
    let push x = value_stack := x :: !value_stack
      
    let push_list xs = value_stack := xs @ !value_stack
      
    let pop () =
      match !value_stack with
      | x :: xs -> (value_stack := xs; x)
      | [] -> runtime_error "stack empty"
      
    let top () =
      match !value_stack with
      | x :: _ -> x
      | [] -> runtime_error "stack empty"
      
    let remove n =
      let rec iter n stack =
        if n <= 0
        then value_stack := stack
        else
          (match stack with
           | [] -> value_stack := []
           | _ :: ys -> iter (n - 1) ys)
      in iter n !value_stack
      
    let get n =
      let rec iter n stack =
        if n <= 0
        then (value_stack := stack; [])
        else
          (match stack with
           | [] -> runtime_error "stack empty"
           | y :: ys -> y :: (iter (n - 1) ys))
      in iter n !value_stack
      
    let get_rev n =
      let rec iter n xs stack =
        if n <= 0
        then (value_stack := stack; xs)
        else
          (match stack with
           | [] -> runtime_error "stack empty"
           | y :: ys -> iter (n - 1) (y :: xs) ys)
      in iter n [] !value_stack
      
    let peek n =
      let res = Array.make n (ref Unbound) in
      let rec iter i stack =
        if i >= n
        then res
        else
          (match stack with
           | [] -> runtime_error "stack empty"
           | y :: ys -> (res.(i) <- y; iter (i + 1) ys))
      in iter 0 !value_stack
      
    let call cont = call_stack := cont :: !call_stack
      
    let return () =
      match !call_stack with
      | c :: cs -> (call_stack := cs; c ())
      | [] -> runtime_error "stack empty"
      
  end
  
(* debugging *)
let rec print_pattern pat =
  match pat with
  | PCAnything -> Printf.printf " _"
  | PCVariable i -> Printf.printf " v%d" i
  | PCNumber n -> Printf.printf " %f" (float_of_num n)
  | PCChar c -> Printf.printf " c%d" c
  | PCSymbol s ->
      Printf.printf " s\"%s\""
        (UString.to_string (Array.to_list (symbol_to_string s)))
  | PCTuple n -> Printf.printf " (%d)" n
  | PCNil -> Printf.printf " []"
  | PCConsList -> Printf.printf " :"
  | PCAssign i -> Printf.printf " =%d" i
  
let print_list p sep l =
  match l with
  | [] -> ()
  | [ x ] -> p x
  | x :: xs -> (p x; List.iter (fun y -> (Printf.printf "%s" sep; p y)) xs)
  
let rec print_partial lvl x =
  match x with
  | Unbound -> Printf.printf " <unbound>"
  | Constraint _ -> Printf.printf " <contraint>"
  | Bool b -> Printf.printf "%s" (if b then " True" else " False")
  | Number n -> Printf.printf " %f" (float_of_num n)
  | Char c -> Printf.printf " '\\x%x'" c
  | Symbol s ->
      Printf.printf " %s"
        (UString.to_string (Array.to_list (symbol_to_string s)))
  | LinForm lin ->
      (Printf.printf " (%f" (float_of_num lin.LinForm.const);
       List.iter
         (fun (b, x) ->
            (Printf.printf " + %f *" (float_of_num b);
             if lvl > 0
             then print_partial (lvl - 1) !x
             else Printf.printf " ..."))
         lin.LinForm.terms;
       Printf.printf ")")
  | Application (_, _, _) -> Printf.printf " <unevaluated>"
  | Primitive1 _ -> Printf.printf " <prim 1>"
  | Primitive2 _ -> Printf.printf " <prim 2>"
  | PrimitiveN (n, _) -> Printf.printf " <prim %d>" n
  | Function (_, n, c) ->
      if lvl > 0
      then
        (Printf.printf " fun %d {\n" n;
         Array.iteri (print_b_cmd (lvl - 1)) c;
         Printf.printf "}\n")
      else Printf.printf " fun %d {...}" n
  | Chain _ -> Printf.printf " <cfun>"
  | Relation (_, _) -> Printf.printf " <rel>"
  | Nil -> Printf.printf " []"
  | List (a, b) ->
      if lvl > 0
      then
        (Printf.printf " [";
         print_partial (lvl - 1) !a;
         (let rec iter x =
            match !x with
            | Nil -> Printf.printf "]"
            | List (a, b) ->
                (Printf.printf ","; print_partial (lvl - 1) !a; iter b)
            | _ -> (Printf.printf " :"; print_partial (lvl - 1) !x)
          in iter b))
      else Printf.printf " [...]"
  | Tuple y ->
      if lvl > 0
      then
        (Printf.printf " (";
         print_list (fun a -> print_partial (lvl - 1) !a) ","
           (Array.to_list y);
         Printf.printf ")")
      else Printf.printf " (...)"
  | Dictionary d ->
      if lvl > 0
      then
        (Printf.printf " <dict";
         SymbolMap.iter
           (fun k v ->
              (Printf.printf " %s"
                 (UString.to_string (Array.to_list (symbol_to_string k)));
               print_partial (lvl - 1) !v))
           d;
         Printf.printf ">")
      else
        (Printf.printf " <dict";
         SymbolMap.iter
           (fun k _ ->
              Printf.printf " %s ..."
                (UString.to_string (Array.to_list (symbol_to_string k))))
           d;
         Printf.printf ">")
  | Opaque _ -> Printf.printf " <opaque>"
and print_bytecode lvl code = Array.iteri (print_b_cmd lvl) code
and print_b_cmd lvl i c =
  match c with
  | BDup -> Printf.printf "%3d: dup\n" i
  | BPop -> Printf.printf "%3d: pop\n" i
  | BPopN n -> Printf.printf "%3d: pop %d\n" i n
  | BConst c ->
      (Printf.printf "%3d: const" i; print_partial lvl c; Printf.printf "\n")
  | BGlobal x ->
      (Printf.printf "%3d: global" i;
       print_partial lvl !x;
       Printf.printf "\n")
  | BVariable (k, l) -> Printf.printf "%3d: var %d %d\n" i k l
  | BFunction (n, c) ->
      (Printf.printf "%3d: fun %d {\n" i n;
       Array.iteri (print_b_cmd lvl) c;
       Printf.printf "}\n")
  | BDictionary syms ->
      (Printf.printf "%3d: dict { " i;
       Array.iter
         (fun s ->
            Printf.printf " %s"
              (UString.to_string (Array.to_list (symbol_to_string s))))
         syms;
       Printf.printf " }\n")
  | BPair -> Printf.printf "%3d: pair\n" i
  | BTuple n -> Printf.printf "%3d: tuple %d\n" i n
  | BSet (k, l) -> Printf.printf "%3d: set %d %d\n" i k l
  | BApply n -> Printf.printf "%3d: apply %d\n" i n
  | BReturn -> Printf.printf "%3d: return\n" i
  | BCondJump off -> Printf.printf "%3d: cond-jump %d\n" i off
  | BJump off -> Printf.printf "%3d: jump %d\n" i off
  | BLocal n -> Printf.printf "%3d: local %d\n" i n
  | BEndLocal -> Printf.printf "%3d: end-local\n" i
  | BMatch1 (p, s, v, off) ->
      (Printf.printf "%3d: match 1 %d %d %d {" i s v off;
       List.iter print_pattern p;
       Printf.printf "}\n")
  | BMatchN (p, s, v, off) ->
      (Printf.printf "%3d: match %d %d %d %d" (Array.length p) i s v off;
       for i = 0 to (Array.length p) - 1 do
         Printf.printf " {";
         List.iter print_pattern p.(i);
         Printf.printf "}"
       done;
       Printf.printf "\n")
  | BUnify -> Printf.printf "%3d: unify\n" i
  | BRaise msg -> Printf.printf "%3d: raise \"%s\"\n" i msg
  
let check_patterns checks stack vars expr =
  let rec iter checks expr used_stack =
    let continue cs =
      match cs with
      | [] -> true
      | _ -> iter cs stack.(used_stack - 1) (used_stack - 1)
    in
      match checks with
      | [] -> true
      | c :: cs ->
          (match c with
           | PCAnything -> continue cs
           | PCVariable i -> (vars.(i) <- expr; continue cs)
           | PCAssign i -> (vars.(i) <- expr; iter cs expr used_stack)
           | PCNumber n ->
               (match !expr with
                | Number i -> if not (eq_num n i) then false else continue cs
                | _ -> false)
           | PCChar c ->
               (match !expr with
                | Char d -> if c <> d then false else continue cs
                | _ -> false)
           | PCSymbol sym ->
               (match !expr with
                | Symbol s -> if sym <> s then false else continue cs
                | _ -> false)
           | PCTuple arity ->
               (match !expr with
                | Tuple xs ->
                    if arity = (Array.length xs)
                    then
                      (for i = 0 to (Array.length xs) - 2 do
                         stack.(used_stack + i) <-
                           xs.(((Array.length xs) - i) - 1)
                       done;
                       iter cs xs.(0) ((used_stack + (Array.length xs)) - 1))
                    else false
                | _ -> false)
           | PCNil -> (match !expr with | Nil -> continue cs | _ -> false)
           | PCConsList ->
               (match !expr with
                | List (x, y) ->
                    (stack.(used_stack) <- y; iter cs x (used_stack + 1))
                | _ -> false))
  in iter checks expr 0
  
let rec binom n k =
  let rec iter k n x =
    if k <= 0 then x else iter (k - 1) (n - 1) (mult_num (num_of_ints n k) x)
  in iter (if (2 * k) > n then n - k else k) n num_one
  
let rec add_unknowns res x y =
  match ((!x), (!y)) with
  | (Number m, Number n) -> res := Number (add_num m n)
  | (LinForm m, Number n) -> res := LinForm (LinForm.add_const m n)
  | (Number m, LinForm n) -> res := LinForm (LinForm.add_const n m)
  | (LinForm m, LinForm n) -> res := LinForm (LinForm.add m n)
  | (List (_, _), Nil) -> res := !x
  | (Nil, List (_, _)) -> res := !y
  | (List (a, b), List (_, _)) ->
      let c = ref Unbound in (res := List (a, c); add_unknowns c b y)
  | (Tuple xs, Tuple ys) ->
      if (Array.length xs) <> (Array.length ys)
      then runtime_error "+: tuples differ in length"
      else
        (let len = Array.length xs in
         let zs = Array.init len create_unbound
         in
           (res := Tuple zs;
            for i = 1 to len do
              add_unknowns zs.(len - i) xs.(len - i) ys.(len - i)
            done))
  | (LinForm lin, Tuple xs) | (Tuple xs, LinForm lin) ->
      let dim = Array.length xs
      in
        if not (eq_num lin.LinForm.const num_zero)
        then runtime_error "+: invalid arguments"
        else
          (let rec iter result terms =
             match terms with
             | [] ->
                 res := Tuple (Array.map (fun l -> ref (LinForm l)) result)
             | (a, y) :: ys ->
                 let z = Array.init dim create_unbound
                 in
                   (forced_unify y (ref (Tuple z));
                    let u =
                      Array.init dim
                        (fun i -> LinForm.add_unknown result.(i) a z.(i))
                    in iter u ys)
           in
             iter
               (Array.init dim
                  (fun i -> LinForm.of_unknown compare_unknowns xs.(i)))
               lin.LinForm.terms)
  | (Unbound, _) ->
      res :=
        LinForm
          (LinForm.add (LinForm.of_unknown compare_unknowns x)
             (LinForm.of_unknown compare_unknowns y))
  | (_, Unbound) ->
      res :=
        LinForm
          (LinForm.add (LinForm.of_unknown compare_unknowns x)
             (LinForm.of_unknown compare_unknowns y))
  | (Constraint _, _) ->
      res :=
        LinForm
          (LinForm.add (LinForm.of_unknown compare_unknowns x)
             (LinForm.of_unknown compare_unknowns y))
  | (_, Constraint _) ->
      res :=
        LinForm
          (LinForm.add (LinForm.of_unknown compare_unknowns x)
             (LinForm.of_unknown compare_unknowns y))
  | (Number n, _) when eq_num n num_zero -> res := !y
  | (* Allow addition of 0 to everything so we *) (_, Number n) when
      eq_num n num_zero -> res := !x
  | (* do not need two versions of lin_form.   *) _ ->
      runtime_error "+: invalid argument"
and sub_unknowns res x y =
  match ((!x), (!y)) with
  | (Number m, Number n) -> res := Number (sub_num m n)
  | (LinForm m, Number n) ->
      res := LinForm (LinForm.add_const m (minus_num n))
  | (Number m, LinForm n) ->
      res := LinForm (LinForm.sub (LinForm.of_num compare_unknowns m) n)
  | (LinForm m, LinForm n) -> res := LinForm (LinForm.sub m n)
  | (Tuple xs, Tuple ys) ->
      if (Array.length xs) <> (Array.length ys)
      then runtime_error "-: I cannot subtract tuples of different length"
      else
        (let len = Array.length xs in
         let zs = Array.init len create_unbound
         in
           (res := Tuple zs;
            for i = 1 to len do
              sub_unknowns zs.(len - i) xs.(len - i) ys.(len - i)
            done))
  | (Unbound, _) ->
      res :=
        LinForm
          (LinForm.add (LinForm.of_unknown compare_unknowns x)
             (LinForm.of_scaled_unknown compare_unknowns num_minus_one y))
  | (_, Unbound) ->
      res :=
        LinForm
          (LinForm.add (LinForm.of_unknown compare_unknowns x)
             (LinForm.of_scaled_unknown compare_unknowns num_minus_one y))
  | _ -> runtime_error "-: invalid argument"
and mul_unknowns res x y =
  match ((!x), (!y)) with
  | (Number m, Number n) -> res := Number (mult_num m n)
  | (Number m, LinForm l) -> res := LinForm (LinForm.scale m l)
  | (LinForm l, Number n) -> res := LinForm (LinForm.scale n l)
  | (LinForm m, LinForm n) ->
      (evaluate_lin_form x m;
       evaluate_lin_form y n;
       (match ((!x), (!y)) with
        | (LinForm _, LinForm _) -> runtime_error "*: non-linear equation"
        | _ -> mul_unknowns res x y))
  | (Number m, Unbound) | (Number m, Constraint _) ->
      res := LinForm (LinForm.of_scaled_unknown compare_unknowns m y)
  | (Unbound, Number n) | (Constraint _, Number n) ->
      res := LinForm (LinForm.of_scaled_unknown compare_unknowns n x)
  | (Number _, Tuple ys) | (Unbound, Tuple ys) | (Constraint _, Tuple ys) ->
      let len = Array.length ys in
      let zs = Array.init len create_unbound
      in
        (res := Tuple zs;
         for i = 1 to len do mul_unknowns zs.(len - i) x ys.(len - i) done)
  | (Tuple xs, Number _) | (Tuple xs, Unbound) | (Tuple xs, Constraint _) ->
      let len = Array.length xs in
      let zs = Array.init len create_unbound
      in
        (res := Tuple zs;
         for i = 1 to len do mul_unknowns zs.(len - i) xs.(len - i) y done)
  | (Tuple xs, Tuple ys) ->
      let len = Array.length xs
      in
        if (Array.length ys) <> len
        then runtime_error "*: tuples differ in length"
        else
          (let zs = Array.init len create_unbound
           in
             (for i = 1 to len do mul_unknowns zs.(i) xs.(i) ys.(i) done;
              let rec iter i lin =
                if i >= len
                then res := LinForm lin
                else
                  iter (i + 1)
                    (LinForm.add lin
                       (LinForm.of_unknown compare_unknowns zs.(i)))
              in iter 0 (LinForm.lin_zero compare_unknowns)))
  | (Number _, Primitive1 f) ->
      res :=
        Primitive1
          (fun a -> let z = ref Unbound in (mul_unknowns z x (ref (f a)); !z))
  | (Number _, Primitive2 f) ->
      res :=
        Primitive2
          (fun a b ->
             let z = ref Unbound in (mul_unknowns z x (ref (f a b)); !z))
  | (Number _, PrimitiveN (ar, f)) ->
      res :=
        PrimitiveN (ar,
          (fun a -> let z = ref Unbound in (mul_unknowns z x (ref (f a)); !z)))
  | (Number _, Function (env, ar, body)) ->
      res :=
        Function (env, ar,
          Array.of_list
            ((Array.to_list body) @
               [ BConst !x; BConst (Primitive2 prim_mul) ]))
  | (_, List (_, _)) -> (*  x * [y,z]  =>  y + x*(z-y) *)
      let points = evaluate_list "*" y
      in
        (match points with
         | [ a ] -> bind_unknown res a
         | [ a; b ] -> (* treat the common case separately *)
             let c = ref Unbound in
             let d = ref Unbound
             in
               (sub_unknowns c b a; mul_unknowns d x c; add_unknowns res a d)
         | a :: b ->
             (match !x with
              | Number t ->
                  let n = (List.length points) - 1 in
                  let s = sub_num num_one t in
                  let (_, lin) =
                    List.fold_left
                      (fun (k, lin) c ->
                         ((k + 1),
                          (LinForm.add lin
                             (LinForm.of_scaled_unknown compare_unknowns
                                (mult_num
                                   (mult_num (binom n k)
                                      (power_num s (num_of_int (n - k))))
                                   (power_num t (num_of_int k)))
                                c))))
                      (1,
                       (LinForm.of_scaled_unknown compare_unknowns
                          (power_num s (num_of_int n)) a))
                      b
                  in res := LinForm lin
              | _ ->
                  runtime_error
                    ("*: invalid argument, expected number but got " ^
                       (type_name !x)))
         | [] -> assert false)
  | _ ->
      runtime_error
        ("*: invalid argument of type " ^
           ((type_name !x) ^ (" and " ^ (type_name !y))))
and div_unknowns res x y =
  match ((!x), (!y)) with
  | (Number m, Number n) -> res := Number (div_num m n)
  | (LinForm l, Number n) ->
      res := LinForm (LinForm.scale (div_num num_one n) l)
  | (Unbound, Number n) ->
      res :=
        LinForm
          (LinForm.of_scaled_unknown compare_unknowns (div_num num_one n) x)
  | (Tuple xs, Number _) ->
      let len = Array.length xs in
      let zs = Array.init len create_unbound
      in
        (res := Tuple zs;
         for i = 1 to len do div_unknowns zs.(len - i) xs.(len - i) y done)
  | (_, LinForm l) ->
      (evaluate_lin_form y l;
       (match !y with
        | Number _ -> div_unknowns res x y
        | _ -> runtime_error "/: invalid argument"))
  | _ -> runtime_error "/: invalid argument"
and prim_add x y = let z = ref Unbound in (add_unknowns z x y; !z)
and prim_sub x y = let z = ref Unbound in (sub_unknowns z x y; !z)
and prim_mul x y = let z = ref Unbound in (mul_unknowns z x y; !z)
and prim_div x y = let z = ref Unbound in (div_unknowns z x y; !z)
and evaluate_lin_form x lin =
  ((* We check for unbound, constraint, and other unknowns. *)
   x := Unbound;
   let rec collect terms =
     match terms with
     | [] ->
         ((LinForm.lin_zero compare_unknowns), num_zero,
          (ref (Number lin.LinForm.const)))
     | (a, y) :: ts ->
         let (lin, coeff, const) = collect ts
         in
           (match !y with
            | Unbound ->
                if identical x y
                then (lin, (add_num coeff a), const)
                else ((LinForm.add_unknown lin a y), coeff, const)
            | Constraint _ -> ((LinForm.add_unknown lin a y), coeff, const)
            | _ ->
                let z1 = ref Unbound in
                let z2 = ref Unbound
                in
                  (mul_unknowns z1 (ref (Number a)) y;
                   add_unknowns z2 const z1;
                   (lin, coeff, z2))) in
   let compute_x x coeff sum =
     if eq_num coeff num_zero
     then x := !sum
     else
       if eq_num coeff num_one
       then
         (let z = ref Unbound
          in (sub_unknowns z sum x; forced_unify z (ref (Number num_zero))))
       else
         mul_unknowns x
           (ref (Number (div_num num_one (sub_num num_one coeff)))) sum in
   let sum = ref Unbound in
   let (lin, coeff, const) = collect lin.LinForm.terms
   in
     (if LinForm.is_constant lin
      then add_unknowns sum const (ref (Number lin.LinForm.const))
      else add_unknowns sum const (ref (LinForm lin));
      compute_x x coeff sum))
and evaluate_list name x =
  match !x with
  | Nil -> []
  | List (a, b) -> a :: (evaluate_list name b)
  | Unbound | Constraint _ -> runtime_error (name ^ ": argument undefined")
  | _ -> runtime_error (name ^ ": invalid argument")
and bind_unknown x y =
  match !y with
  | Unbound -> let c = Constraint [ x; y ] in (x := c; y := c)
  | Constraint c ->
      let us = add_constraint x c in
      let new_c = Constraint us in List.iter (fun z -> z := new_c) us
  | LinForm lin ->
      let a = LinForm.coefficient lin x
      in
        if eq_num a num_zero
        then x := !y
        else
          (let l =
             LinForm.sub lin (LinForm.of_scaled_unknown compare_unknowns a x)
           in
             if eq_num a num_one
             then
               (x := Unbound;
                forced_unify (ref (LinForm l)) (ref (Number num_zero)))
             else
               x :=
                 LinForm
                   (LinForm.scale (div_num num_one (sub_num num_one a)) l))
  | _ -> x := !y
and forced_unify x y =
  if not (unify x y)
  then
    runtime_error
      ("unification error: " ^ ((type_name !x) ^ (" and " ^ (type_name !y))))
  else ()
and unify x y =
  let set_unknowns c v = List.iter (fun x -> x := v) c
  in
    match ((!x), (!y)) with
    | (Unbound, _) -> (bind_unknown x y; true)
    | (_, Unbound) -> (bind_unknown y x; true)
    | (Constraint a, Constraint b) ->
        let c = merge_constraints a b
        in (set_unknowns c (Constraint c); true)
    | (Constraint a, _) -> (set_unknowns a !y; true)
    | (_, Constraint b) -> (set_unknowns b !x; true)
    | (Bool a, Bool b) -> a = b
    | (Char a, Char b) -> a = b
    | (Symbol a, Symbol b) -> a = b
    | (Nil, Nil) -> true
    | (List (a1, a2), List (b1, b2)) -> (unify a1 b1) && (unify a2 b2)
    | (Number a, Number b) -> eq_num a b
    | (Number a, LinForm lin) ->
        let x = ref Unbound
        in
          (evaluate_lin_form x lin;
           (match !x with
            | Number b -> eq_num b a
            | LinForm lin ->
                (match lin.LinForm.terms with
                 | [ (c, z) ] ->
                     unify z
                       (ref
                          (Number (div_num (sub_num a lin.LinForm.const) c)))
                 | (c, z) :: _ ->
                     unify z
                       (ref
                          (LinForm
                             (LinForm.add_const
                                (LinForm.scale
                                   (div_num (minus_num num_one) c)
                                   (LinForm.remove_first_term lin))
                                a)))
                 | _ -> assert false)
            | _ -> assert false))
    | (LinForm lin, Number a) ->
        let x = ref Unbound
        in
          (evaluate_lin_form x lin;
           (match !x with
            | Number b -> eq_num b a
            | LinForm lin ->
                (match lin.LinForm.terms with
                 | [ (c, z) ] ->
                     unify z
                       (ref
                          (Number (div_num (sub_num a lin.LinForm.const) c)))
                 | (c, z) :: _ ->
                     unify z
                       (ref
                          (LinForm
                             (LinForm.add_const
                                (LinForm.scale
                                   (div_num (minus_num num_one) c)
                                   (LinForm.remove_first_term lin))
                                a)))
                 | _ -> assert false)
            | _ -> assert false))
    | (LinForm a, LinForm b) ->
        let x = ref Unbound in
        let y = ref Unbound in
        let z = ref Unbound
        in
          (evaluate_lin_form x a;
           evaluate_lin_form y b;
           let c =
             (match !x with
              | Number n -> LinForm.of_num compare_unknowns n
              | LinForm l -> l
              | _ -> assert false) in
           let d =
             (match !y with
              | Number n -> LinForm.of_num compare_unknowns n
              | LinForm l -> l
              | _ -> assert false)
           in
             (evaluate_lin_form z
                (LinForm.lin_comb num_one c (minus_num num_one) d);
              (match !z with
               | Number c -> eq_num c num_zero
               | LinForm lin ->
                   (match lin.LinForm.terms with
                    | [ (c, u) ] ->
                        unify u
                          (ref
                             (Number
                                (div_num (minus_num lin.LinForm.const) c)))
                    | (c, u) :: _ ->
                        unify u
                          (ref
                             (LinForm
                                (LinForm.scale
                                   (div_num (minus_num num_one) c)
                                   (LinForm.remove_first_term lin))))
                    | _ -> assert false)
               | _ -> assert false)))
    | (Tuple a, Tuple b) ->
        if (Array.length a) <> (Array.length b)
        then false
        else
          (let rec iter i =
             if i >= (Array.length a)
             then true
             else if unify a.(i) b.(i) then iter (i + 1) else false
           in iter 0)
    | (Dictionary a, Dictionary b) ->
        let l0 = map_to_list a in
        let l1 = map_to_list b in
        let rec iter l0 l1 =
          (match (l0, l1) with
           | ([], []) -> true
           | ([], _) -> false
           | (_, []) -> false
           | ((k0, v0) :: kv0, (k1, v1) :: kv1) ->
               if k0 <> k1
               then false
               else if unify v0 v1 then iter kv0 kv1 else false)
        in iter l0 l1
    | (Primitive1 a, Primitive1 b) -> a == b
    | (Primitive2 a, Primitive2 b) -> a == b
    | (PrimitiveN (a1, a2), PrimitiveN (b1, b2)) -> (a1 = b1) && (a2 == b2)
    | (Function (a1, a2, a3), Function (b1, b2, b3)) ->
        (a1 == b1) && ((a2 = b2) && (a3 == b3))
    | (Relation (a1, a2), Relation (b1, b2)) -> (a1 = b1) && (a2 = b2)
    | (Opaque a, Opaque b) -> (Opaque.same_type a b) && (Opaque.unify a b)
    | _ -> false
  
let rec execute_code env bytecode pc =
  (if !tracing_bytecode
   then
     (Printf.printf "[%d/%d]" (List.length !Stack.value_stack)
        (List.length !Stack.call_stack);
      if pc < (Array.length bytecode)
      then print_b_cmd 3 pc bytecode.(pc)
      else Printf.printf "%3d: stoped\n" pc;
      flush stdout)
   else ();
   if pc >= (Array.length bytecode)
   then ()
   else
     (match bytecode.(pc) with
      | BDup ->
          (Stack.push (Stack.top ()); execute_code env bytecode (pc + 1))
      | BPop -> (ignore (Stack.pop ()); execute_code env bytecode (pc + 1))
      | BPopN n -> (Stack.remove n; execute_code env bytecode (pc + 1))
      | BConst c -> (Stack.push (ref c); execute_code env bytecode (pc + 1))
      | BGlobal x -> (Stack.push x; execute_code env bytecode (pc + 1))
      | BVariable (d, i) ->
          (Stack.push (Environment.lookup env d i);
           execute_code env bytecode (pc + 1))
      | BFunction (a, c) ->
          (Stack.push (ref (Function (env, a, c)));
           execute_code env bytecode (pc + 1))
      | BDictionary syms ->
          let rec iter i d =
            if i >= (Array.length syms)
            then
              (Stack.push (ref (Dictionary d));
               execute_code env bytecode (pc + 1))
            else
              (let v = Stack.pop ()
               in iter (i + 1) (SymbolMap.add syms.(i) v d))
          in iter 0 SymbolMap.empty
      | BPair ->
          let a = Stack.pop () in
          let b = Stack.pop ()
          in
            (Stack.push (ref (List (a, b)));
             execute_code env bytecode (pc + 1))
      | BTuple n ->
          let elements = Stack.get n
          in
            (Stack.push (ref (Tuple (Array.of_list elements)));
             execute_code env bytecode (pc + 1))
      | BSet (d, i) ->
          (Environment.set env d i (Stack.pop ());
           execute_code env bytecode (pc + 1))
      | BApply n ->
          let f = Stack.pop () in execute_function env !f n bytecode (pc + 1)
      | BReturn -> Stack.return ()
      | BCondJump off ->
          let p = Stack.pop ()
          in
            (match !p with
             | Bool true -> execute_code env bytecode (pc + 1)
             | Bool false -> execute_code env bytecode (pc + off)
             | _ ->
                 runtime_error
                   ("boolean expected but got " ^ ((type_name !p) ^ ".")))
      | BJump off -> execute_code env bytecode (pc + off)
      | BLocal n ->
          execute_code (Environment.push_unbound env n) bytecode (pc + 1)
      | BEndLocal -> execute_code (Environment.pop env) bytecode (pc + 1)
      | BMatch1 (pat, stack, vars, off) ->
          let arg = Stack.top () in
          let v = Array.init vars create_unbound in
          let s = Array.init stack create_unbound
          in
            if check_patterns pat s v arg
            then execute_code (Environment.push env v) bytecode (pc + 1)
            else
              if off <> 0
              then execute_code env bytecode (pc + off)
              else runtime_error "matching error"
      | BMatchN (pats, stack, vars, off) ->
          let n = Array.length pats in
          let args = Stack.peek n in
          let v = Array.init vars create_unbound in
          let s = Array.init stack create_unbound in
          let rec iter i =
            if i >= n
            then execute_code (Environment.push env v) bytecode (pc + 1)
            else
              if check_patterns pats.(i) s v args.(i)
              then iter (i + 1)
              else
                if off <> 0
                then execute_code env bytecode (pc + off)
                else runtime_error "matching error"
          in iter 0
      | BUnify ->
          let x = Stack.pop () in
          let y = Stack.pop () in
          let _ = unify x y in
            execute_code env bytecode (pc + 1)
      | BRaise msg -> runtime_error msg))
and execute_unary_function env contents n bytecode pc =
  if n = 1
  then (Stack.push contents; execute_code env bytecode pc)
  else execute_function env !contents (n - 1) bytecode pc
and execute_function env f n bytecode pc =
  match f with
  | Primitive1 p ->
      let x = Stack.pop ()
      in execute_unary_function env (ref (p x)) n bytecode pc
  | Primitive2 p ->
      if n = 2
      then
        (let x = Stack.pop () in
         let y = Stack.pop ()
         in (Stack.push (ref (p x y)); execute_code env bytecode pc))
      else
        if n = 1
        then
          (let x = Stack.pop ()
           in
             (Stack.push (ref (Application (f, 1, [ x ])));
              execute_code env bytecode pc))
        else
          (let x = Stack.pop () in
           let y = Stack.pop ()
           in execute_function env (p x y) (n - 2) bytecode pc)
  | PrimitiveN (k, p) ->
      if n = k
      then
        (let args = Stack.get n
         in (Stack.push (ref (p args)); execute_code env bytecode pc))
      else
        if n < k
        then
          (let args = Stack.get n
           in
             (Stack.push (ref (Application (f, k - n, args)));
              execute_code env bytecode pc))
        else
          (let args = Stack.get k
           in execute_function env (p args) (n - k) bytecode pc)
  | Function (e, k, code) ->
      if n = k
      then
        (Stack.call (fun () -> execute_code env bytecode pc);
         execute_code e code 0)
      else
        if n < k
        then
          (let args = Stack.get n
           in
             (Stack.push (ref (Application (f, k - n, args)));
              execute_code env bytecode pc))
        else
          (Stack.call
             (fun () ->
                let res = Stack.pop ()
                in execute_function env !res (n - k) bytecode pc);
           execute_code e code 0)
  | Application (f, k, args) ->
      if n = k
      then
        (Stack.push_list args;
         execute_function env f (n + (List.length args)) bytecode pc)
      else
        if n < k
        then
          (let args2 = Stack.get n
           in
             (Stack.push (ref (Application (f, k - n, args2 @ args)));
              execute_code env bytecode pc))
        else
          (Stack.call
             (fun () ->
                let res = Stack.pop ()
                in execute_function env !res (n - k) bytecode pc);
           Stack.push_list args;
           execute_function env f (n + (List.length args)) bytecode pc)
  | (* access methods *) Dictionary dict ->
      let x = Stack.pop ()
      in
        (match !x with
         | Symbol s ->
             (try
                let y = SymbolMap.find s dict
                in execute_unary_function env y n bytecode pc
              with
              | Not_found ->
                  runtime_error
                    ("entry " ^
                       ((UString.to_string
                           (Array.to_list (symbol_to_string s)))
                          ^ " not found in dictionary")))
         | _ ->
             runtime_error
               ("type error: symbol expected but got " ^ (type_name !x)))
  | Tuple ys ->
      let x = Stack.pop ()
      in
        (match !x with
         | Number k ->
             if is_integer_num k
             then
               (let i = int_of_num k
                in
                  if (i >= 0) && (i < (Array.length ys))
                  then execute_unary_function env ys.(i) n bytecode pc
                  else runtime_error "index out of range")
             else runtime_error "non-integral index"
         | _ ->
             runtime_error
               ("type error: integer expected but got " ^ (type_name !x)))
  | List (_, _) ->
      let x = Stack.pop ()
      in
        (match !x with
         | Number k ->
             if is_integer_num k
             then
               (let rec iter lst i =
                  match lst with
                  | Nil -> runtime_error "index out of range"
                  | List (y, z) ->
                      if i = 0
                      then execute_unary_function env y n bytecode pc
                      else
                        if i > 0
                        then iter !z (i - 1)
                        else runtime_error "index out of range"
                  | _ -> runtime_error "malformed list"
                in iter f (int_of_num k))
             else runtime_error "non-integral index"
         | _ ->
             runtime_error
               ("type error: integer expected but got " ^ (type_name !x)))
  | Opaque y ->
      let x = Stack.pop () in
      let z = Opaque.apply y x in execute_unary_function env z n bytecode pc
  | Nil -> runtime_error "index out of range"
  | Unbound | Constraint _ -> runtime_error "application of unknown function"
  | _ ->
      runtime_error
        ("type error: function expected but got " ^ ((type_name f) ^ "!"))
  
let execute code args =
  (Stack.clear ();
   Stack.push_list args;
   execute_code Environment.empty code 0;
   Stack.pop ())
  
let evaluate_num name x =
  match !x with
  | Number n -> n
  | LinForm l ->
      (evaluate_lin_form x l;
       (match !x with
        | Number n -> n
        | _ ->
            runtime_error
              (name ^ (": number expected but got " ^ (type_name !x)))))
  | _ ->
      runtime_error (name ^ (": number expected but got " ^ (type_name !x)))
  
let evaluate_opaque opaque_name unwrapper name x =
  match !x with
  | Opaque y ->
      (try unwrapper y
       with
       | Opaque.Type_error ->
           runtime_error
             (name ^
                (": " ^
                   (opaque_name ^ (" expected but got " ^ (type_name !x))))))
  | Unbound | Constraint _ -> runtime_error (name ^ ": argument not defined")
  | _ ->
      runtime_error
        (name ^
           (": " ^ (opaque_name ^ (" expected but got " ^ (type_name !x)))))
  

